﻿// Jinx AJAX Framework
// Copyright (C) 2008 Blake Hegerle
//
// This program is free software: you can redistribute it and/or modify
// it under the terms of the GNU General Public License as published by
// the Free Software Foundation, either version 3 of the License, or
// (at your option) any later version.
//
// This program is distributed in the hope that it will be useful,
// but WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
// GNU General Public License for more details.
//
// You should have received a copy of the GNU General Public License
// along with this program.  If not, see <http://www.gnu.org/licenses/>.

using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using Core;

namespace Formality.FormalSystem.Reasoning.VariableRenaming
{
    public class Search : IJustificationSearch
    {
        public Search(Proposition From, Proposition To)
        {
            this.From = From; this.To = To;

            Map = new Dictionary<Variable, Variable>();
        }

        public Justification Perform()
        {
            if (Descend(From, To))
                return new Justification(Map);
            return null;
        }

        #region IJustificationSearch Members

        Reasoning.Justification IJustificationSearch.Perform()
        {
            return Perform();
        }

        #endregion

        private Proposition From, To;
        private readonly Dictionary<Variable, Variable> Map;

        private bool Descend(Proposition f, Proposition t)
        {
            /*
             * Check if the operators are the same
             *  Check if the variables can be consistently renamed
             *      Check if the operands recursively admit this substitution
             *          Check for variable capture
             */
            if (f.Operator == t.Operator)
                if (f.Variables.SequenceEqual(t.Variables, AdmitSubstitution))
                    if (f.Operands.SequenceEqual(t.Operands, Descend))
                        if (!Capture(f, t))
                            return true;

            return false;
        }

        private bool Capture(Proposition From, Proposition To)
        {
            if (From.Type == PropType.Binder)
            {
                var FromVar = new Binder(From).Variable;
                var ToVar = new Binder(To).Variable;

                Map.Remove(FromVar);

                return Map.Any(Sub => Sub.Value == ToVar);
            }

            return false;
        }

        private bool AdmitSubstitution(Variable From, Variable To)
        {
            Variable OldSubstitution;

            if (Map.TryGetValue(From, out OldSubstitution))
                return OldSubstitution == To;

            Map[From] = To;
            return true;
        }
    }
}
